\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:Id, $T$:Type, $v$:$T$, ${\it ks}$:(Knd List),\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]fpf{-}compatible(Id; $x$.Type; id{-}deq; ${\it ds}$; fpf{-}single($x$; $T$))
\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex]($T$)
\-\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ ${\it ks}$) $\Rightarrow$ ($\uparrow$isrcv($k$)) $\Rightarrow$ ($i$ = destination(lnk($k$))))
\\[0ex]$\Rightarrow$ normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ normal{-}da\=\{i:l\}\+
\\[0ex](${\it da}$)
\-\\[0ex]$\Rightarrow$ R{-}realizes\=\{i:l\}\+
\\[0ex](\=R{-}state{-}var{-}init($i$; ${\it ds}$; ${\it da}$; $x$; $T$; $v$; ${\it ks}$; ${\it tr}$);\+
\\[0ex]${\it es}$.(es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ \=(es{-}dtype(${\it es}$; $i$; $x$; $T$)\+
\\[0ex]c$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.((\=es{-}after(${\it es}$; $x$; $e$)\+
\\[0ex]=
\\[0ex]es{-}trans{-}state{-}from\{i:l\}(${\it es}$;${\it ks}$;${\it tr}$;$v$;es{-}init(${\it es}$;$e$);$e$)
\\[0ex]$\in$ $T$)
\-\\[0ex]$\wedge$ (($\uparrow$es{-}first(${\it es}$; $e$)) $\Rightarrow$ (es{-}when(${\it es}$; $x$; $e$) = $v$ $\in$ $T$)))))))
\-\-\-\-
\end{tabbing}